import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes
import Lock

class MailBox(simsym.tstruct(
		msgs = symtypes.tdict(simsym.SInt, ptypes.MBOXMSG),
		head = simsym.SInt,
		tail = simsym.SInt,
		lck = Lock.Lock
                )):
	def _declare_assumptions(self, assume):
		super(MailBox, self)._declare_assumptions(assume)
	
	@model.methodwrap(l = Lock.Lock)
	def INIT(self, l):
		self.lck = l
		self.head = 1
		self.tail = 1
		return
	
	@model.methodwrap(m = ptypes.MBOXMSG)
	def PostMessage(self, m):
		self.lck.Lock()
		self.msgs._map[self.tail] = m
		self.tail = self.tail + 1
		self.lck.Unlock()
		return True

	@model.methodwrap()
	def HaveMessages(self):
		self.lck.Lock()
		ret = self.msgs.empty
		self.lck.Unlock()
		return not ret

	@model.methodwrap()
	def NextMessage(self):
		self.lck.Lock()
		m = self.msgs._map[self.head]
		self.head = self.head + 1
		self.lck.Unlock()
		return m

model_class = MailBox

